T:Type, a, b:(T List).
(||a|| = ||b||  )  (i:. (i < ||a||)  (a[i] = b[i]  T))  (a = b) 

latex

ProofTree

Definitions	, t  T, P  Q, x:A. B(x), Y, ||as||, P  Q, P  Q, True, T, False, A, P & Q, A  B, , ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), l[i]
Lemmas	length wf1, select wf, nat wf, length cons, non neg length, length wf2, select cons tl, le wf, squash wf